Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(app(sort,f),g),nil)  → nil
2:    app(app(app(sort,f),g),app(app(cons,x),y))  → app(app(app(app(insert,f),g),app(app(app(sort,f),g),y)),x)
3:    app(app(app(app(insert,f),g),nil),y)  → app(app(cons,y),nil)
4:    app(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → app(app(cons,app(app(f,x),y)),app(app(app(app(insert,f),g),z),app(app(g,x),y)))
5:    app(app(max,0),y)  → y
6:    app(app(max,x),0)  → x
7:    app(app(max,app(s,x)),app(s,y))  → app(app(max,x),y)
8:    app(app(min,0),y)  → 0
9:    app(app(min,x),0)  → 0
10:    app(app(min,app(s,x)),app(s,y))  → app(app(min,x),y)
11:    app(asort,z)  → app(app(app(sort,min),max),z)
12:    app(dsort,z)  → app(app(app(sort,max),min),z)
There are 25 dependency pairs:
13:    APP(app(app(sort,f),g),app(app(cons,x),y))  → APP(app(app(app(insert,f),g),app(app(app(sort,f),g),y)),x)
14:    APP(app(app(sort,f),g),app(app(cons,x),y))  → APP(app(app(insert,f),g),app(app(app(sort,f),g),y))
15:    APP(app(app(sort,f),g),app(app(cons,x),y))  → APP(app(insert,f),g)
16:    APP(app(app(sort,f),g),app(app(cons,x),y))  → APP(insert,f)
17:    APP(app(app(sort,f),g),app(app(cons,x),y))  → APP(app(app(sort,f),g),y)
18:    APP(app(app(app(insert,f),g),nil),y)  → APP(app(cons,y),nil)
19:    APP(app(app(app(insert,f),g),nil),y)  → APP(cons,y)
20:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(app(cons,app(app(f,x),y)),app(app(app(app(insert,f),g),z),app(app(g,x),y)))
21:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(cons,app(app(f,x),y))
22:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(app(f,x),y)
23:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(f,x)
24:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(app(app(app(insert,f),g),z),app(app(g,x),y))
25:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(app(app(insert,f),g),z)
26:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(app(g,x),y)
27:    APP(app(app(app(insert,f),g),app(app(cons,x),z)),y)  → APP(g,x)
28:    APP(app(max,app(s,x)),app(s,y))  → APP(app(max,x),y)
29:    APP(app(max,app(s,x)),app(s,y))  → APP(max,x)
30:    APP(app(min,app(s,x)),app(s,y))  → APP(app(min,x),y)
31:    APP(app(min,app(s,x)),app(s,y))  → APP(min,x)
32:    APP(asort,z)  → APP(app(app(sort,min),max),z)
33:    APP(asort,z)  → APP(app(sort,min),max)
34:    APP(asort,z)  → APP(sort,min)
35:    APP(dsort,z)  → APP(app(app(sort,max),min),z)
36:    APP(dsort,z)  → APP(app(sort,max),min)
37:    APP(dsort,z)  → APP(sort,max)
The approximated dependency graph contains one SCC: {13-15,17,18,20,22-28,30,32,33,35,36}.
Tyrolean Termination Tool  (114.58 seconds)   ---  May 3, 2006